structure LCoqize2 = (*Coqize in low level*)
struct 
  structure Asm = Assem
  structure A = Assert
  (* added by lge 2006.05.14 --begin *)
  structure P = Proof2
  structure E = ErrorMsg
  structure T = Temp
  structure R = A_Reduce
  (* added by lge 2006.05.14 --end *)
  fun nullemit str:string = str  
  

  fun precPterm p =
      let fun prec P.True = 100
            | prec P.Eax = 100
            | prec P.Ebx = 100
            | prec P.Ecx = 100
            | prec P.Edx = 100
            | prec P.Esi = 100
            | prec P.Edi = 100
            | prec P.Ebp = 100
            | prec P.Esp = 100
            | prec (P.IntNum(i)) = 100
            | prec (P.Lab(i)) = 100
            | prec (P.AddrN(i)) = 100
            | prec (P.Var(s)) = 100
            | prec (P.Asst(s)) = 100
            | prec (P.St(rf, hp)) = 100
            | prec (P.Ch(ch)) = 100
            | prec (P.Iseq(is)) = 100
            | prec (P.ChTy(ty)) = 100
            | prec (P.Times(p1, p2)) = 75
            | prec (P.Plus(p1, p2)) = 50
            | prec (P.Minus(p1, p2)) = 50
            | prec (P.Gt(p1, p2)) = 40
            | prec (P.Ge(p1, p2)) = 40
            | prec (P.Lt(p1, p2)) = 40
            | prec (P.Le(p1, p2)) = 40
            | prec (P.Eq(p1, p2)) = 30
            | prec (P.Ne(p1, p2)) = 30
            | prec (P.And(p1, p2)) = 20
            | prec (P.Or(p1, p2)) = 10
            | prec (P.Not(p)) = 100
            | prec (P.App(p1, p2)) = 5
            | prec (P.Abs((s,t), p)) = 1
            | prec (P.Ex((s,t), p)) = 1
      in  prec p
      end

  fun pr_st emit st = 
      let fun pr A.Rf = ("R",1)
	    | pr A.Hp = ("H",2)
	    | pr (A.Upd(st1,e0,e1)) = 
(*	      let val str_st1 = pr(st1)
		  val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in (print("need more work in update node");
		  "Upd("^str_st1^", "^str_e0^", "^str_e1^")")
	      end*)
	      let val str_st1 = pr(st1)
		  val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in ((fn 1 => "(updateR ("^(#1 str_st1)^") ("^str_e0^") ("^str_e1^"))"
		   | 2 => "(hwrite ("^(#1 str_st1)^") ("^str_e0^") ("^str_e1^"))"
		   | _ => (print("never happen\n");"")) (#2 str_st1), (#2 str_st1))
	      end 
      in pr(st)
      end

  and pr_exp emit e = 
      let fun pr (A.IntNum(i)) = 
	      if(i<0)
	      then ("(-"^Int.toString(Int.abs(i))^")")
	      else Int.toString(i)
	    | pr (A.Addr(ad)) = 
	      if(ad<0)
	      then ("(-"^Int.toString(Int.abs(ad))^")")
	      else Int.toString(ad)
	    | pr (A.Plus(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^"+"^str_e1^")"
	      end 
	    | pr (A.Minus(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^"-"^str_e1^")"
	      end 
	    | pr (A.Times(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in str_e0^"*"^str_e1
	      end 
	    | pr (A.Sel(st0,e0)) = 
(*	      let val str_st0 = pr_st nullemit st0
		  val str_e0 = pr_exp nullemit e0
	      in str_st0^"["^str_e0^"]"
	      end*)
	      let val str_st0 = pr_st nullemit st0
		  val str_e0 = pr_exp nullemit e0
	      in (fn 1 => "(lookupR "^(#1 str_st0)^" "^str_e0^")"
		   | 2 => "(hread "^(#1 str_st0)^" "^str_e0^")"
		   | _ => (print("never happen\n");"")) (#2 str_st0)
	      end
	    | pr A.Eax = "eax"
	    | pr A.Ebx = "ebx"
	    | pr A.Ecx = "ecx"
	    | pr A.Edx = "edx"
	    | pr A.Esi = "esi"
	    | pr A.Edi = "edi"
	    | pr A.Esp = "esp"
	    | pr A.Ebp = "ebp"
	    | pr _ = ""
      in emit (pr e)
      end

  fun space 0 = ""
    | space i = " "^(space (i-1))  

  fun pr_etype emit t =
      let fun pr A.Int = "Z" 
            | pr A.Label = "addr"
            | pr A.Wild = "_"
      in  pr t
      end
  
  fun pr_prop i emit pp = 
      let fun pr A.True = (space i) ^ "True"
	    | pr (A.Imply(p0,p1)) = 
	      let val str_p0 = pr_prop i nullemit p0
		  val str_p1 = pr_prop (i+2) nullemit p1
	      in str_p0^"->\n"^str_p1
	      end
	    | pr (A.Not(p0)) = 
	      let val str_p0 = pr_prop 0 nullemit p0
	      in (space i) ^ "(~"^str_p0^")"
	      end
	    | pr (A.And(p0,p1)) = 
	      let val str_p0 = pr_prop 0 nullemit p0
		  val str_p1 = pr_prop 0 nullemit p1
	      in (space i) ^ "("^str_p0^")/\\("^str_p1^")"
	      end
	    | pr (A.Or(p0,p1)) = 
	      let val str_p0 = pr_prop 0 nullemit p0
		  val str_p1 = pr_prop 0 nullemit p1
	      in (space i) ^ "("^str_p0^")\\/("^str_p1^")"
	      end
	    | pr (A.Gt(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in (space i) ^"("^str_e0^")>("^str_e1^")"
	      end
	    | pr (A.Ge(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in (space i) ^ "("^str_e0^")>=("^str_e1^")"	      
	      end
	    | pr (A.Lt(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in  (space i) ^ "("^str_e0^")<("^str_e1^")"	      
	      end
	    | pr (A.Le(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in  (space i) ^ "("^str_e0^")<=("^str_e1^")"	      
	      end
	    | pr (A.Eq(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in (space i) ^ "("^str_e0^")=("^str_e1^")"	      
	      end
	    | pr (A.Ne(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in (space i) ^ "("^str_e0^")<>("^str_e1^")"	      
	      end
            | pr (A.Ex((s, t), p)) =
              let val t' = pr_etype nullemit t
                  val p' = pr_prop (i+2) nullemit p
              in  (space i) ^ "exists "^s^" : "^t'^",\n("^p'^")"
              end
            | pr (A.InDom(e, st)) =
              let val e' = pr_exp nullemit e
                  val (st', n) = pr_st nullemit st
              in  if n=2 
                  then (space i)^ "hindom ("^e'^") ("^st'^")"
                  else (raise Fail "InDom not in heap!"; "bogus")
              end
      in emit (pr pp)
      end

  (* added by lge 2006.5.14 --begin *)

  fun pr_asst i emit asst =
      let val state = (A.Rf, A.Hp)
          val prop = R.red_prop (asst state)
	  val asst' = (space i) ^ "fun s:(heap * rfile) => let (H, R) := s in \n"^  (*WIP*)
                      (pr_prop (i+2) nullemit prop)
      in  emit asst'
      end

  fun pr_reg emit r =
      let fun pr (Asm.Eax) = "eax"
            | pr (Asm.Ebx) = "ebx"
            | pr (Asm.Ecx) = "ecx"
            | pr (Asm.Edx) = "edx"
            | pr (Asm.Esi) = "esi"
            | pr (Asm.Edi) = "edi"
            | pr (Asm.Esp) = "esp"
            | pr (Asm.Ebp) = "ebp"
      in  emit (pr r)
      end

  fun filt (#".") = #"_"
    | filt c = c

  fun lkup [] name = NONE
    | lkup ((name1, lab)::l) name = if name1 = name
                                    then SOME(lab)
                                    else lkup l name
  fun pr_int i = if(i<0)
	         then ("(-"^Int.toString(Int.abs(i))^")")
	         else Int.toString(i)
  fun pr_instr emit ins specs =
      let fun pr (Asm.Addr(r1, r2)) = 
              let val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2
              in  "addr "^r1'^" "^r2'
              end
            | pr (Asm.Addz(i, r)) =
              let val i' = if(i<0)
	                   then ("(-"^Int.toString(Int.abs(i))^")")
	                   else Int.toString(i)
                  val r' = pr_reg nullemit r
              in "addz "^i'^" "^r'
              end
            | pr (Asm.Subr(r1, r2)) = 
              let val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2
              in  "subr "^r1'^" "^r2'
              end
            | pr (Asm.Subz(i, r)) =
              let val i' = if(i<0)
	                   then ("(-"^Int.toString(Int.abs(i))^")")
	                   else Int.toString(i)
                  val r' = pr_reg nullemit r
              in "subz "^i'^" "^r'
              end
            | pr (Asm.Mulr(r1, r2)) = 
              let val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2
              in  "mulr "^r1'^" "^r2'
              end
            | pr (Asm.Mulz(i, r)) =
              let val i' = if(i<0)
	                   then ("(-"^Int.toString(Int.abs(i))^")")
	                   else Int.toString(i)
                  val r' = pr_reg nullemit r
              in "mulz "^i'^" "^r'
              end
            | pr (Asm.Div(r)) =
              let val r' = pr_reg nullemit r
              in  "div "^r'
              end         
            | pr (Asm.Push(r)) =
              let val r' = pr_reg nullemit r
              in  "push "^r'
              end
            | pr (Asm.Pop(r)) =
              let val r' = pr_reg nullemit r
              in  "pop "^r'
              end
            | pr (Asm.Beq (r1, r2, l)) =
              let val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2
                  val l' = String.map filt l
                  val labnum' = case (lkup specs l')
                                 of SOME(l) => l
                                  | NONE => (raise Fail "There is no such label!"; 0)
                  val labnum = pr_int labnum'   
              in  "beq "^r1'^" "^r2'^" "^labnum
              end
            | pr (Asm.Bgt (r1, r2, l)) =
              let val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2
                  val l' = String.map filt l
                  val labnum' = case (lkup specs l')
                                 of SOME(l) => l
                                  | NONE => (raise Fail "There is no such label!"; 0)
                  val labnum = pr_int labnum'   
              in  "bgt "^r1'^" "^r2'^" "^labnum
              end
            | pr (Asm.Bge (r1, r2, l)) =
              let val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2
                  val l' = String.map filt l
                  val labnum' = case (lkup specs l')
                                 of SOME(l) => l
                                  | NONE => (raise Fail "There is no such label!"; 0)
                  val labnum = pr_int labnum'   
              in  "bge "^r1'^" "^r2'^" "^labnum
              end
            | pr (Asm.Beqi(i, r, l)) =
              let val i' = pr_int i
                  val r' = pr_reg nullemit r
                  val l' = String.map filt l
                  val labnum' = case (lkup specs l')
                                 of SOME(l) => l
                                  | NONE => (raise Fail "There is no such label!"; 0)
                  val labnum = pr_int labnum'
              in  "beqi "^i'^" "^r'^" "^labnum
              end
            | pr (Asm.Bgti(i, r, l)) =
              let val i' = pr_int i
                  val r' = pr_reg nullemit r
                  val l' = String.map filt l
                  val labnum' = case (lkup specs l')
                                 of SOME(l) => l
                                  | NONE => (raise Fail "There is no such label!"; 0)
                  val labnum = pr_int labnum'
              in  "bgti "^i'^" "^r'^" "^labnum
              end
            | pr (Asm.Xchg(r1, r2)) =
              let val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2 
              in  "xchg "^r1'^" "^r2'
              end
            | pr (Asm.Leal(l, r)) =
              let val l' = String.map filt l
                  val labnum' = case (lkup specs l')
                                 of SOME(l) => l
                                  | NONE => (raise Fail "There is no such label!"; 0)
                  val labnum = pr_int labnum'
                  val r' = pr_reg nullemit r
              in  "leal "^labnum^" "^r'
              end
            | pr (Asm.Leab(i, r1, r2)) =
              let val i' = pr_int i
                  val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2
              in  "leab "^i'^" "^r1'^" "^r2'
              end
            | pr (Asm.Movr(r1, r2)) =
              let val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2
              in  "movr "^r1'^" "^r2'
              end
            | pr (Asm.Movz(i, r)) =
              let val i' = pr_int i
                  val r' = pr_reg nullemit r
              in  "movz "^i'^" "^r'
              end
            | pr (Asm.Movld(i, r1, r2)) =
              let val i' = pr_int i
                  val r1' = pr_reg nullemit r1
                  val r2' = pr_reg nullemit r2
              in  "movld "^i'^" "^r1'^" "^r2'
              end
            | pr (Asm.Movst(r1, i, r2)) =
              let val r1' = pr_reg nullemit r1
                  val i' = pr_int i
                  val r2' = pr_reg nullemit r2
              in  "movst "^r1'^" "^i'^" "^r2'
              end
            (* WIP should raise Fail*)
            | pr _ = (print "can not print theses instructions.\n"; "other instructions")
      in  emit (pr ins)
      end

  fun pr_specs asst =
      let val newspecs = ref []
          val coqspecs = ref []
          fun get_hd s = String.substring(s, 0, 3)
          fun pr [] = ()
            | pr ({lab= l, asst = (SOME(a))} ::ls) =
              let val asstname = String.map filt l  (*WIP*)
                  val asst = pr_asst 2 nullemit a
                  val asstcoq = "Definition "^asstname^"_asst :state -> Prop := \n"^asst^".\n"
                  val size = String.size l
              in  (if size <=3 orelse (get_hd l) <>"..A" 
                   then let val newlab = T.newNum()
                        in  newspecs := (asstname, newlab)::(!newspecs)
                        end
                   else ());
                  coqspecs := asstcoq :: (!coqspecs);
                  pr ls
              end
            | pr ({lab = l, asst = NONE}::ls) =(* raise Fail ("Impossible! lack of specification."; ()) *)
              let val asstname = String.map filt l  (*WIP*)
                  val size = String.size l
                  val asstcoq = "Definition "^asstname^"_asst:state -> Prop := To be implemented.\n"
              in  (if size <= 3 orelse (get_hd l) <> "..A"
                   then let val newlab = T.newNum()
                        in  newspecs := (asstname, newlab)::(!newspecs)
                        end
                   else ());
                  coqspecs := asstcoq ::(!coqspecs);
                  pr ls
              end
      in  pr asst;
          (!newspecs, !coqspecs)
      end

  fun pr_heapspec' i newspec = 
      let fun pr [] = (space i) ^ "emptyCT"
            | pr ((asst, lab)::specs) = 
              let val specs' = pr_heapspec' (i+2) specs
                  val lab' = Int.toString(lab)
              in  (space i)^ "(consCT "^lab'^" "^asst^"_asst \n "^specs'^")"
              end
      in  pr newspec
      end
  fun pr_heapspec specname specs = 
      let val cdhptp = pr_heapspec' 2 specs
      in  "Definition "^specname^": codeheapty :=\n"^cdhptp^"."
      end


  fun  pr_chty i emit chtp = 
       let fun pr [] = (space i) ^ "emptyCT"
             | pr ((asst, l):: ls) =
               let val ls' = pr_chty (i+2) nullemit ls
                   val lab = Int.toString(l)
               in  "(consCT "^lab^" "^asst^"_asst \n "^ls'^")"
               end
       in  emit (pr chtp)
       end

  fun pr_iseq ii emit is specs= 
      let fun pr [] = (raise Fail "must be ended with jmp, call or ret\n"; "other ended instructions") (* WIP should raise Fail *)
            | pr [Asm.Jmp(l)] =
              let val l' = String.map filt l
                  val labnum' = case (lkup specs l')
                                 of SOME(l) => l
                                  | NONE => (raise Fail "There is no such label!"; 0)
                  val labnum = pr_int labnum'
              in  (space ii) ^ "(jmp "^" "^labnum^")"
              end
            | pr [Asm.Call(l)] =
              let val l' = String.map filt l
                  val labnum' = case (lkup specs l')
                                 of SOME(l) => l
                                  | NONE => (raise Fail "There is no such label!"; 0)
                  val labnum = pr_int labnum'
              in  (space ii) ^ "(call "^" "^labnum^")"
              end
            | pr [Asm.Ret] = (space ii) ^ "ret"
            | pr (i::is'') =
              let val i' = pr_instr nullemit i specs
                  val is' = pr_iseq (ii+2) nullemit is'' specs
              in  (space ii) ^ "(seq ("^i'^") \n "^is'^")"
              end
      in  emit (pr is)
      end

  fun pr_ch emit ch specs = "" (*WIP*)


  fun pr_pterm i oprec l emit specs pt =
      let val iprec = precPterm pt
          val paren = iprec < oprec
          fun pr (P.Abs((id, atype), pterm)) =
              let val ptype = pr_atype (i+10) nullemit atype specs
              in  if l>=1 
                  then "\n"^(space (i+2)) ^ (if paren then "(" else "")^
                       "fun ("^id^": "^ptype^")=>"^
                       (pr_pterm (i+2) iprec 0 nullemit specs pterm)^
                       (if paren then "(" else "")
                  else ""^(if paren then "(" else "")^
                       "fun ("^id^": "^ptype^")=>"^
                       (pr_pterm i iprec (l+1) nullemit specs pterm)^
                       (if paren then "(" else "")
              end
(*
              let val ptype = pr_atype nullemit atype specs
                  val ppterm = pr_pterm (i+2) nullemit specs pterm
              in  (space i)^ "fun ("^id^":"^ptype^") =>\n"^ppterm
              end
*)
            | pr (P.App(pterm1, pterm2)) =
              let fun gethead (P.Var(s)) = s
                    | gethead (P.App(p1, p2)) = gethead p1
                    | gethead _ = "Error"
                  val s = gethead pterm1
                  val shead = String.substring(s, 0, 1)
              in  if l >=3 
                  then "\n" ^ (space (i+2)) ^ (if paren then "(" else "")^
                       (if (s = "infer") orelse (shead = "h") orelse (shead ="I") 
                        then (pr_pterm (i+2) iprec 0 nullemit specs pterm1)^" "^
                             (pr_pterm (i+2) iprec 3 nullemit specs pterm2)
                        else (pr_pterm (i+2) iprec 0 nullemit specs pterm1)^" "^
                             (pr_pterm (i+2) iprec 0 nullemit specs pterm2))^
                       (if paren then ")" else "")
                  else ""^ (if paren then "(" else "")^
                       (if (s = "infer") orelse (shead = "h") orelse (shead ="I")
                        then (pr_pterm i iprec 0 nullemit specs pterm1)^" "^
                             (pr_pterm i iprec 3 nullemit specs pterm2)
                        else (pr_pterm i iprec 0 nullemit specs pterm1)^" "^
                             (pr_pterm i iprec 0 nullemit specs pterm2))^
                       (if paren then ")" else "")
              end
(*
              let val ppterm1 = pr_pterm i nullemit specs pterm1
                  val ppterm2 = pr_pterm (i+2) nullemit specs pterm2
              in  ppterm1 ^ "\n" ^ ppterm2 
              end
*)
            | pr (P.Var(s)) = if l>=3 
                              then "\n"^(space (i+2)) ^ s
                              else s
            | pr (P.IntNum(ii)) = if l>=3 
                                  then "\n"^(space (i+2)) ^ (pr_int ii)
                                  else pr_int ii
            | pr (P.Lab(ii)) =  if l>=3 
                                then "\n"^(space (i+2)) ^ (pr_int ii)
                                else pr_int ii
            | pr (P.AddrN(ii)) =  if l>=3 
                                  then "\n"^(space (i+2)) ^ (pr_int ii)
                                  else pr_int ii
            | pr (P.True) = if l>=3 
                            then "\n"^(space (i+2)) ^ "True"
                            else "True"
            | pr (P.Eax) =  if l>=3 
                            then "\n"^(space (i+2)) ^ "eax"
                            else "eax"
            | pr (P.Ebx) =  if l>=3 
                            then "\n"^(space (i+2)) ^ "ebx"
                            else "ebx"
            | pr (P.Ecx) =  if l>=3 
                            then "\n"^(space (i+2)) ^ "ecx"
                            else "ecx"
            | pr (P.Edx) =  if l>=3 
                            then "\n"^(space (i+2)) ^ "edx"
                            else "edx"
            | pr (P.Esi) =  if l>=3 
                            then "\n"^(space (i+2)) ^ "esi"
                            else "esi"
            | pr (P.Edi) =   if l>=3 
                            then "\n"^(space (i+2)) ^ "edi"
                            else "edi"     
            | pr (P.Esp) =  if l>=3 
                            then "\n"^(space (i+2)) ^ "esp"
                            else "esp"
            | pr (P.Ebp) =  if l>=3 
                            then "\n"^(space (i+2)) ^ "ebp"
                            else "ebp"
            | pr (P.Plus(e1, e2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs e1)^
                   " + "^
                   (pr_pterm (i+2) iprec 0 nullemit specs e2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs e1)^
                   " + "^
                   (pr_pterm i iprec 0 nullemit specs e2)^
                   (if paren then ")" else "")
(* 
              let val e1' = pr_pterm 0 nullemit specs e1
                  val e2' = pr_pterm 0 nullemit specs e2
              in  (space i) ^ "(" ^ e1' ^ " + " ^ e2' ^ ")"
              end
*)
            | pr (P.Minus(e1, e2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs e1)^
                   " - "^
                   (pr_pterm (i+2) iprec 0 nullemit specs e2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs e1)^
                   " - "^
                   (pr_pterm i iprec 0 nullemit specs e2)^
                   (if paren then ")" else "")
(*
              let val e1' = pr_pterm 0 nullemit specs e1
                  val e2' = pr_pterm 0 nullemit specs e2
              in  (space i) ^ "(" ^ e1' ^ " - " ^ e2' ^ ")"
              end
*)
            | pr (P.Times(e1, e2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs e1)^
                   " * "^
                   (pr_pterm (i+2) iprec 0 nullemit specs e2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs e1)^
                   " * "^
                   (pr_pterm i iprec 0 nullemit specs e2)^
                   (if paren then ")" else "")
(*
              let val e1' = pr_pterm 0 nullemit specs e1 
                  val e2' = pr_pterm 0 nullemit specs e2
              in  (space i) ^ e1' ^ " * " ^ e2'
              end
*)
            | pr (P.Gt(e1, e2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs e1)^
                   " > "^
                   (pr_pterm (i+2) iprec 0 nullemit specs e2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs e1)^
                   " > "^
                   (pr_pterm i iprec 0 nullemit specs e2)^
                   (if paren then ")" else "")
(*
	      let val e1' = pr_pterm 0 nullemit specs e1
		  val e2' = pr_pterm 0 nullemit specs e2
	      in (space i) ^ "("^e1'^")>("^e2'^")"
	      end
*)
            | pr (P.Ge(e1, e2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs e1)^
                   " >= "^
                   (pr_pterm (i+2) iprec 0 nullemit specs e2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs e1)^
                   " >= "^
                   (pr_pterm i iprec 0 nullemit specs e2)^
                   (if paren then ")" else "")
(*
	      let val e1' = pr_pterm 0 nullemit specs e1
		  val e2' = pr_pterm 0 nullemit specs e2
	      in (space i) ^ "("^e1'^")>=("^e2'^")"
	      end
*)
            | pr (P.Lt(e1, e2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs e1)^
                   " < "^
                   (pr_pterm (i+2) iprec 0 nullemit specs e2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs e1)^
                   " < "^
                   (pr_pterm i iprec 0 nullemit specs e2)^
                   (if paren then ")" else "")
(*
	      let val e1' = pr_pterm 0 nullemit specs e1
		  val e2' = pr_pterm 0 nullemit specs e2
	      in (space i) ^ "("^e1'^")<("^e2'^")"
	      end
*)
            | pr (P.Le(e1, e2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs e1)^
                   " <= "^
                   (pr_pterm (i+2) iprec 0 nullemit specs e2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs e1)^
                   " <= "^
                   (pr_pterm i iprec 0 nullemit specs e2)^
                   (if paren then ")" else "")
(*
	      let val e1' = pr_pterm 0 nullemit specs e1
		  val e2' = pr_pterm 0 nullemit specs e2
	      in  (space i) ^ "("^e1'^")<=("^e2'^")"
	      end
*)
            | pr (P.Eq(e1, e2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs e1)^
                   " = "^
                   (pr_pterm (i+2) iprec 0 nullemit specs e2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs e1)^
                   " = "^
                   (pr_pterm i iprec 0 nullemit specs e2)^
                   (if paren then ")" else "")
(*
	      let val e1' = pr_pterm 0 nullemit specs e1
		  val e2' = pr_pterm 0 nullemit specs e2
	      in  (space i) ^  "("^e1'^")=("^e2'^")"
	      end
*)
            | pr (P.Ne(e1, e2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs e1)^
                   " <> "^
                   (pr_pterm (i+2) iprec 0 nullemit specs e2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs e1)^
                   " <> "^
                   (pr_pterm i iprec 0 nullemit specs e2)^
                   (if paren then ")" else "")
(*
	      let val e1' = pr_pterm 0 nullemit specs e1
		  val e2' = pr_pterm 0 nullemit specs e2
	      in (space i) ^ "("^e1'^")<>("^e2'^")"
	      end
*)
            | pr (P.And(p1, p2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs p1)^
                   " /\\ "^
                   (pr_pterm (i+2) iprec 0 nullemit specs p2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs p1)^
                   " /\\ "^
                   (pr_pterm i iprec 0 nullemit specs p2)^
                   (if paren then ")" else "")
(*
	      let val p1' = pr_pterm 0 nullemit specs p1
		  val p2' = pr_pterm 0 nullemit specs p2
	      in (space i) ^ "("^p1'^")/\\("^p2'^")"
	      end
*)
            | pr (P.Or(p1, p2)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^
                   (pr_pterm (i+2) iprec 0 nullemit specs p1)^
                   " \\/ "^
                   (pr_pterm (i+2) iprec 0 nullemit specs p2)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^
                   (pr_pterm i iprec 0 nullemit specs p1)^
                   " \\/ "^
                   (pr_pterm i iprec 0 nullemit specs p2)^
                   (if paren then ")" else "")
(*
              let val p1' = pr_pterm 0 nullemit specs p1
                  val p2' = pr_pterm 0 nullemit specs p2
              in  (space i) ^ "("^p1'^")\\/("^p2'^")"
              end
*)
            | pr (P.Not(p)) =
              if l>=3 
              then "\n"^(space (i+2))^ (if paren then "(" else "")^"~"^
                   (pr_pterm (i+2) iprec 0 nullemit specs p)^
                   (if paren then "(" else "")
              else ""^ (if paren then "(" else "")^"~"^
                   (pr_pterm i iprec 0 nullemit specs p)^
                   (if paren then ")" else "")
(*
              let val p' = pr_pterm 0 nullemit specs p
              in  (space i) ^ "(~"^p'^")"
              end
*)
            | pr (P.ChTy(chtp)) = 
              let val chtp' = pr_chty (i+2) nullemit chtp
              in  chtp'
              end
            | pr (P.Iseq(is)) = 
              let val is' = pr_iseq (i+2) nullemit is specs
              in  if l>=3 
                  then "\n" ^ is'
                  else is'
              end
            | pr (P.Ch(ch)) =  (*WIP*)
              let val ch' = pr_ch nullemit ch specs
              in  if l>=3 
                  then "\n" ^ ch'
                  else ch'
              end
            | pr (P.St(rf, hp)) =
              if l>=3 
              then "\n"^(space (i+2))^ "(" ^
                   (pr_pterm (i+2) iprec 0 nullemit specs rf)^
                   ", "^
                   (pr_pterm (i+2) iprec 0 nullemit specs hp)^ ")"
              else ""^"("^
                   (pr_pterm i iprec 0 nullemit specs rf)^
                   ", "^
                   (pr_pterm i iprec 0 nullemit specs hp)^ ")"
(*
              let val rf' = pr_pterm 0 nullemit specs rf 
                  val hp' = pr_pterm 0 nullemit specs hp
              in (space i) ^ "("^rf'^", "^hp'^")"
              end
*)
            | pr (P.Asst(asst)) =
              let val asst' = (String.map filt asst)^"_asst"
              (*pr_asst i nullemit asst*) 
              in  if l>=3 
                  then "\n"^(space (i+2)) ^ asst'
                  else asst'
              end
(*
              in  (space i) ^ asst'
              end
*)

            | pr (P.Ex((id, atype), pterm)) =
              let val ptype = pr_atype (i+10) nullemit atype specs
              in  if l>=1 
                  then "\n"^(space (i+2)) ^ (if paren then "(" else "")^
                       "exists ("^id^": "^ptype^"), "^
                       (pr_pterm (i+2) iprec 0 nullemit specs pterm)^
                       (if paren then "(" else "")
                  else ""^(if paren then "(" else "")^
                       "exists ("^id^": "^ptype^"), "^
                       (pr_pterm i iprec (l+1) nullemit specs pterm)^
                       (if paren then "(" else "")
              end

      in emit (pr pt)
      end

  and pr_atype i emit at specs= 
      let fun pr (P.Int) = "int"
            | pr (P.Label) = "lab"
            | pr (P.Addr) = "addr"
            | pr (P.Hp) = "heap"
            | pr (P.Rf) = "rfile"
            | pr (P.Sta) = "state"
            | pr (P.Reg) = "reg"
            | pr (P.CB) = "iseq"
            | pr (P.CT) = "codeheapty"
            | pr (P.CH) = "codeheap"
            | pr (P.Assert) = "assert"
            | pr (P.Prop(pt)) = 
              let val pt' = pr_pterm i ~1 0 nullemit specs pt
              in  pt'
              end
            | pr (P.Wild) = "_"
      in  emit (pr at)
      end 
  (* added by lge 2006.5.14 --end *)


  fun pr_tactic speclist t=
      let fun pr (P.T_proof) = "Proof"
            | pr (P.T_qed) = "Qed"
            | pr (P.T_auto) = "auto"
	    | pr (P.T_unfold(str)) = "unfold "^str
            | pr (P.T_apply (rule, [])) =
              "apply "^rule
            | pr (P.T_apply(rule, arglist)) = 
              let val str_p = String.concat 
		                  (List.map (fn (pname, pt) => 
				                ("("^pname^":="^(String.map filt pt)^"_asst)")) arglist)
              in "apply "^rule^" with "^str_p
              end
            | pr (P.T_exact(p)) = 
              let val substr = pr_pterm 4 ~1 3 nullemit speclist p
              in "exact ("^
                 substr^
                 ")"
              end
            | pr (P.T_intros []) = 
              "intros"
            | pr (P.T_intros arglist) =
              let val str_p = String.concat
                                  (List.map (fn(s) =>" "^s) arglist)
              in "intros"^str_p
              end
            | pr (P.T_inversion_clear(s, [])) =
              "inversion_clear "^ s
            | pr (P.T_inversion_clear(s, arglist)) = 
              let fun pr [] = ""
                    | pr [s] = s
                    | pr (s::al) = s ^" "^(pr al)
                  val str_p = pr arglist
              in "inversion_clear "^ s ^ " as ["^str_p ^ "]"
              end
            | pr (P.T_or(t1, t2)) = 
              let val t1' = pr t1
                  val t2' = pr t2
              in  t1'^" || "^ t2'
              end
            | pr (P.T_seq(t1, t2)) =
              let val t1' = pr t1
                  val t2' = pr t2
              in t1'^"; "^t2'
              end
            | pr (P.T_para tl) = 
              let fun p [] = (raise Fail "no such case."; "bogus")
                    | p [t] = (raise Fail "no such case"; "bogus")
                    | p [t1, t2] = (pr t1)^" | "^(pr t2)
                    | p (t::l) = (pr t)^" | "^(p l)
              in "[ "^(p tl)^" ]"
              end
            | pr (P.T_split) = "split"
      in  "  "^(pr t)^".\n"
      end

  (* added by lge 2006.5.14 --begin *)
  (* assertion to Coq format*)
  fun asst2coq2' emit (label, bkasst, pterm) specs= 
      let val label' = 
	      (fn (#".") => (String.substring(label,1,
					      ((String.size label)-1)))
		| _ => label) (String.sub(label, 0))
	  val state = (A.Rf,A.Hp)
	  val prop = bkasst state
	  val str' = pr_prop 2 nullemit prop
	  val str = "Lemma Asst_"^label'^": forall (R:rfile) (H:heap),\n"
		    ^str'^".\n"
          val term = pterm state
          val pstr' = pr_pterm 2 ~1 3 nullemit specs term
          val pstr = "Proof.\n"^
                     "exact(\n"^
                     "fun (R:rfile)=> (fun (H:heap) => "^ pstr'^")\n"^
                     ").\n"^
                     "Qed.\n"
          val str_pstr = str ^ pstr
      in emit str_pstr
      end 
  
  fun asst2coq2 specs bkinf = asst2coq2' nullemit bkinf specs

  fun coqhead () = "Require Export asm.\n"^
                   "Require Import ZArith.\n"^
                   "Open Scope Z_scope.\n\n"
  (* added by lge 2006.5.14 --end *)

  (* assertion to Coq format*)
  fun asst2coq' emit (label, bkasst) = 
      let val label' = 
	      (fn (#".") => (String.substring(label,1,
					      ((String.size label)-1)))
		| _ => label) (String.sub(label, 0))
	  val state = (A.Rf,A.Hp)
	  val prop = bkasst state
	  val str' = pr_prop 2 nullemit prop
	  val str = "Lemma Asst_"^label'^": forall (R:rfile) (H:heap),\n"
		    ^str'^".\n"
      in emit str
      end 
  
  fun asst2coq bkinf = asst2coq' nullemit bkinf


  (* forward to Coq format*)
  fun fw2coq isdata spec instr = 
      (fn (Asm.Label (l,_)) => 
	  if isdata
	  then ""
	  else let val asst = A.getspec l spec 
	       in case asst
		   of NONE => ""
		    | SOME a => asst2coq(l,a)
	       end
	| _ => "") instr

end
